package mac5739.experimento;

import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
import java.util.Random;

import org.apache.commons.lang.StringUtils;

import bcontractor.api.SATReasoner;
import bcontractor.base.CountingReasoner;
import bcontractor.partialmeet.PartialMeetContractionOperator;
import bcontractor.partialmeet.RemainderSetOperator;
import bcontractor.partialmeet.SelectionFunction;
import bcontractor.partialmeet.selection.FullSelectionFunction;
import bcontractor.propositional.PropositionalSentence;
import bcontractor.propositional.factories.ArbitraryClauseFactory;
import bcontractor.propositional.factories.ContractionCase;
import bcontractor.propositional.factories.ContractionCaseFactory;
import bcontractor.propositional.factories.HornClauseFactory;
import bcontractor.propositional.factories.PropositionalSentenceSetFactory;
import bcontractor.propositional.factories.SentenceFactory;
import bcontractor.propositional.factories.SentenceSetFactory;
import bcontractor.propositional.minisat.MiniSatReasoner;

/**
 * Experimento para o projeto 2 da disciplina de MAC5739 - Laboratório de Inteligência Artificial
 * 
 * @author lundberg
 * 
 */
public class Experiment {

	private static final int RUNS_PER_CONFIGURATION = 50;

	private SATReasoner<PropositionalSentence> reasoner;

	private File outputFile;

	public static void main(String... args) throws Exception {
		new Experiment().run();
	}

	public void run() throws Exception {
		outputFile = new File("experiment.out");
		outputFile.delete();
		outputFile.createNewFile();
		reasoner = new MiniSatReasoner();
		Random random = new Random(System.currentTimeMillis());
		String header = join("clauseType", "nVariables", "nClauses", "alphaSize", "minClauseSize", "maxClauseSize", "reasonerAccessCount", "runningTime",
		"timeSpentReasoning", "timePerReasoning");
		print("nVariables from 5 to 10\n");
		print(header);
		for (int nVariables = 20; nVariables < 40; nVariables++) {
			int nClauses = 100;
			int alphaSize = 10;
			int minClauseSize = 5;
			int maxClauseSize = 10;
			runExperiment(new Random(random.nextLong()), nVariables, nClauses, alphaSize, minClauseSize, maxClauseSize);
		}
		print("nClauses from 30 to 40\n");
		print(header);
		for (int nClauses = 60; nClauses < 100; nClauses++) {
			int nVariables = 20;
			int alphaSize = 10;
			int minClauseSize = 5;
			int maxClauseSize = 10;
			runExperiment(new Random(random.nextLong()), nVariables, nClauses, alphaSize, minClauseSize, maxClauseSize);
		}
		print("alphaSize from 2 to 8\n");
		print(header);
		for (int alphaSize = 10; alphaSize < 15; alphaSize++) {
			int nVariables = 25;
			int nClauses = 100;
			int minClauseSize = 5;
			int maxClauseSize = 10;
			runExperiment(new Random(random.nextLong()), nVariables, nClauses, alphaSize, minClauseSize, maxClauseSize);
		}
		print("minClauseSize from 1 to 5, maxClauseSize from 5 to 9\n");
		print(header);
		for (int minClauseSize = 5; minClauseSize < 10; minClauseSize++) {
			int nVariables = 25;
			int nClauses = 100;
			int alphaSize = 15;
			int maxClauseSize = minClauseSize + 5;
			runExperiment(new Random(random.nextLong()), nVariables, nClauses, alphaSize, minClauseSize, maxClauseSize);
		}
	}

	/**
	 * Executes the experimento on the given parameters
	 * 
	 * @param nVariables nVariables
	 * @param nClauses nClauses
	 * @param alphaSize alphaSize
	 * @param minClauseSize minClauseSize
	 * @param maxClauseSize maxClauseSize
	 */
	private void runExperiment(final Random random, final int nVariables, final int nClauses, final int alphaSize, final int minClauseSize,
			final int maxClauseSize) {
		ContractionCaseFactory<PropositionalSentence> arbitraryCase = createArbitraryContractionCaseFactory(random, nVariables, nClauses, alphaSize, minClauseSize, maxClauseSize);
		run(nVariables, nClauses, alphaSize, minClauseSize, maxClauseSize, arbitraryCase, "arbitrary");
		ContractionCaseFactory<PropositionalSentence> hornCase = createHornContractionCaseFactory(random, nVariables, nClauses, alphaSize, minClauseSize, maxClauseSize);
		run(nVariables, nClauses, alphaSize, minClauseSize, maxClauseSize, hornCase, "horn");
	}

	private void run(final int nVariables, final int nClauses,
			final int alphaSize, final int minClauseSize,
			final int maxClauseSize,
			ContractionCaseFactory<PropositionalSentence> caseFactory,
			String baseType) {
		double runningTime = 0;
		double reasonerAccessCount = 0;
		double timeSpentReasoning = 0;
		for(int i = 0; i < RUNS_PER_CONFIGURATION; i++) {
			CountingReasoner<PropositionalSentence> countingReasoner = new CountingReasoner<PropositionalSentence>(reasoner);
			runningTime += runContraction(countingReasoner, caseFactory.create());
			reasonerAccessCount += countingReasoner.getCount();
			timeSpentReasoning += countingReasoner.getTimeSpent();
			System.out.print(".");
		}
		print(join(baseType, nVariables, nClauses, alphaSize, minClauseSize, maxClauseSize, reasonerAccessCount / RUNS_PER_CONFIGURATION, runningTime / RUNS_PER_CONFIGURATION,
				timeSpentReasoning / RUNS_PER_CONFIGURATION, timeSpentReasoning / reasonerAccessCount));
	}

	private String join(Object... data) {
		return StringUtils.join(data, ";") + "\n";
	}

	private long runContraction(SATReasoner<PropositionalSentence> reasoner, ContractionCase<PropositionalSentence> arbitraryCase) {
		RemainderSetOperator<PropositionalSentence> remainder = new SingleElementRemainderSetOperator<PropositionalSentence>(reasoner);
		SelectionFunction<PropositionalSentence> selection = new FullSelectionFunction<PropositionalSentence>();
		PartialMeetContractionOperator<PropositionalSentence> contraction = new PartialMeetContractionOperator<PropositionalSentence>(remainder, selection);
		long start = System.currentTimeMillis();
		contraction.eval(arbitraryCase.getSentences(), arbitraryCase.getSentence());
		return System.currentTimeMillis() - start;
	}

	private ContractionCaseFactory<PropositionalSentence> createArbitraryContractionCaseFactory(Random random, int nVariables, int nClauses, int alphaSize,
			int minClauseSize, int maxClauseSize) {
		SentenceFactory<PropositionalSentence> alphaFactory = new ArbitraryClauseFactory(random, nVariables, alphaSize, alphaSize);
		SentenceFactory<PropositionalSentence> clauseFactory = new ArbitraryClauseFactory(random, nVariables, minClauseSize, maxClauseSize);
		SentenceSetFactory<PropositionalSentence> sentenceSetFactory = new PropositionalSentenceSetFactory(clauseFactory, nVariables, nClauses);
		ContractionCaseFactory<PropositionalSentence> contractionCaseFactory = new ContractionCaseFactory<PropositionalSentence>(sentenceSetFactory,
				alphaFactory, reasoner);
		return contractionCaseFactory;
	}

	private ContractionCaseFactory<PropositionalSentence> createHornContractionCaseFactory(Random random, int nVariables, int nClauses, int alphaSize, int minClauseSize,
			int maxClauseSize) {
		SentenceFactory<PropositionalSentence> alphaFactory = new HornClauseFactory(random, nVariables, alphaSize, alphaSize);
		SentenceFactory<PropositionalSentence> clauseFactory = new HornClauseFactory(random, nVariables, minClauseSize, maxClauseSize);
		SentenceSetFactory<PropositionalSentence> sentenceSetFactory = new PropositionalSentenceSetFactory(clauseFactory, nVariables, nClauses);
		ContractionCaseFactory<PropositionalSentence> contractionCaseFactory = new ContractionCaseFactory<PropositionalSentence>(sentenceSetFactory,
				alphaFactory, reasoner);
		return contractionCaseFactory;
	}

	private void print(String message) {
		System.out.println(message);
		try {
			FileWriter writer = new FileWriter(outputFile, true);
			writer.write(message);
			writer.close();
		} catch (IOException e) {
			// OK
		}
	}
}
